\begin{tabbing}
val{-}axiom(\=$E$;$V$;$M$;${\it info}$;${\it pred?}$;\+
\\[0ex]${\it init}$;${\it Trans}$;${\it Choose}$;
\\[0ex]${\it Send}$;${\it val}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$.\+\+
\\[0ex]islocal(kind(${\it info}$;$e$))
\\[0ex]$\Rightarrow$ \=isl(\=${\it Choose}$\+\+
\\[0ex](loc(${\it info}$;$e$)
\\[0ex],act(kind(${\it info}$;$e$))
\\[0ex],state\_when($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$)))
\-\\[0ex]\& \=${\it val}$($e$)\+
\\[0ex]$=$
\\[0ex]outl(\=${\it Choose}$\+
\\[0ex](loc(${\it info}$;$e$)
\\[0ex],act(kind(${\it info}$;$e$))
\\[0ex],state\_when($e$;${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$)))
\-\\[0ex]$\in$ $V$(loc(${\it info}$;$e$),act(kind(${\it info}$;$e$))))
\-\-\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]isrcv(kind(${\it info}$;$e$))
\\[0ex]$\Rightarrow$ (\=$\langle$lnk(kind(${\it info}$;$e$))\+
\\[0ex]$,\,$tag(kind(${\it info}$;$e$))
\\[0ex]$,\,$(${\it val}$($e$))$\rangle$ $\in$ \=${\it Send}$\+
\\[0ex](loc(${\it info}$;sender(${\it info}$;$e$))
\\[0ex],kind(${\it info}$;sender(${\it info}$;$e$))
\\[0ex],${\it val}$(sender(${\it info}$;$e$))
\\[0ex],state\_when(sender(${\it info}$;$e$);${\it info}$;${\it pred?}$;${\it init}$;${\it Trans}$;${\it val}$)) $\in$ Msg($M$)))
\-\-\-\-
\end{tabbing}